// ***** This file is automatically generated from NonZero.java.jpp

package daikon.inv.unary.scalar;

import daikon.*;
import daikon.inv.*;
import daikon.inv.unary.sequence.*;
import daikon.inv.binary.sequenceScalar.*;
import daikon.derive.unary.*;

import java.util.*;
import java.util.logging.Logger;
import java.util.logging.Level;
import plume.*;

/**
 * Represents double scalars that are non-zero.  Prints as <samp>x != 0</samp>.
 */

public class NonZeroFloat
  extends SingleFloat
{
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20030822L;

  // Variables starting with dkconfig_ should only be set via the
  // daikon.config.Configuration interface.
  /**
   * Boolean.  True iff NonZeroFloat invariants should be considered.
   **/
  public static boolean dkconfig_enabled = true;

  /**
   * Determines whether non-null is obvious on 'this' variables.  While
   * 'this' can never be null (making the invariant vacuous), object-client
   * relations can exist between this and references to the class.  The client
   * references can be null, which makes this invariant interesting.
   */
  private static boolean this_non_null_obvious = true;

  /** Debug tracer. **/
  public static final Logger debug = Logger.getLogger("daikon.inv.unary.scalar.NonZeroFloat");

  /** Maximum value ever used for max-min in confidence calculation. **/
  static long range_max = 50;

  private NonZeroFloat(PptSlice ppt) {
    super(ppt);
  }

  private /*@Prototype*/ NonZeroFloat() {
    super();
  }

  private static /*@Prototype*/ NonZeroFloat proto;

  /** Returns the prototype invariant for NonZeroFloat **/
  public static /*@Prototype*/ NonZeroFloat get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ NonZeroFloat ();
    return (proto);
  }

  /** returns whether or not this invariant is enabled **/
  public boolean enabled() {
    return dkconfig_enabled;
  }

  /** Make sure the NonZero make sense on these vars **/
  public boolean instantiate_ok (VarInfo[] vis) {

    if (!valid_types(vis))
      return (false);

    if (vis[0].aux.getFlag (VarInfoAux.IS_STRUCT) ||
        !vis[0].aux.getFlag (VarInfoAux.HAS_NULL))
      return (false);

    return (true);
  }

  /** instantiate an invariant on the specified slice **/
  public NonZeroFloat instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new NonZeroFloat (slice);
  }

  private String zero(OutputFormat format) {

    {
      return "0";
    }
  }

  public String format_using(OutputFormat format) /*@Prototype*/ {
    // // var() fails for prototype invariants
    // if (ppt == null) {
    //   return "Prototype NonZeroFloat invariant (ppt == null)";
    // }

    String name = var().name_using(format);

    if (format.isJavaFamily()) {

        return "daikon.Quant.fuzzy.ne(" + name + ", " + zero(format) + ")";
    }

    if ((format == OutputFormat.DAIKON)
        || (format == OutputFormat.ESCJAVA))
    {
      return name + " != " + zero(format);
    }

    if (format == OutputFormat.SIMPLIFY) {
      return "(NEQ " + var().simplifyFixup(name) + " " + zero(format) + ")";
    }

    return format_unimplemented(format);
  }

  public InvariantStatus check_modified(double v, int count) {
    if (v == 0) {
      return InvariantStatus.FALSIFIED;
    } else {
      return InvariantStatus.NO_CHANGE;
    }
  }

  public InvariantStatus add_modified(double v, int count) {
    InvariantStatus status = check_modified(v, count);
    if (status == InvariantStatus.FALSIFIED) {
      if (logOn())
        log (debug, "falsified (value = " + v + ")");
    } // else if (logDetail())
      // log ("add_modified (" + v + ")");
    return status;
  }

  /**
   * Returns whether or not the variable is a pointer.
   */
  private boolean is_pointer() {
    return (ppt.var_infos[0].file_rep_type == ProglangType.HASHCODE);
  }

  protected double computeConfidence() {
    return 1 - computeProbability();
  }

  // used by computeConfidence
  protected double computeProbability() {
    assert ! falsified;
    // This method works by looking at all sample values and
    // calculating the probability that they were all non-zero by
    // chance (assuming a uniform distribution).  If the variable is
    // not a pointer, the range used is the observed range from sample
    // data.  Further observed constraints are used to change the
    // returned probability, such as all samples being congruent some
    // modulus.

    ValueSet.ValueSetFloat vs = (ValueSet.ValueSetFloat) ppt.var_infos[0].get_value_set();

    // If greater than or less than 0, the bounds invariant will be more
    // interesting
    if (!is_pointer() && ((vs.min() > 0) || (vs.max() < 0))) {

      // Maybe just use 0 as the min or max instead, and see what happens:
      // see whether the "nonzero" invariant holds anyway.  (Perhaps only
      // makes sense to do if the {Lower,Upper}Bound invariant doesn't imply
      // the non-zeroness.)  In that case, do still check for no values yet
      // received.
      return Invariant.PROBABILITY_UNJUSTIFIED;
    } else {
      double range;
      if (is_pointer()) {
        range = 3;
      } else {
        long modulus = 1;
        {
          Modulus mi = Modulus.find(ppt);
          if (mi != null) {
            modulus = mi.modulus;
          }
        }
        // Perhaps I ought to check that it's possible (given the modulus
        // constraints) for the value to be zero; otherwise, the modulus
        // constraint implies non-zero.
        range = (vs.max() - vs.min() + 1) / modulus;
      }
      if ((range_max != 0) && (range > range_max)) {
        range = range_max;
      }

      double probability_one_elt_nonzero = 1 - 1.0/range;
      // This could underflow; so consider doing
      //   double log_probability = self.samples*math.log(probability);
      // then calling Math.exp (if the value is in the range that wouldn't
      // cause underflow).
      // return Math.pow(probability_one_elt_nonzero, ppt.num_mod_samples());
      return Math.pow(probability_one_elt_nonzero, ppt.num_samples());
    }
  }

  public /*@Nullable*/ DiscardInfo isObviousStatically(VarInfo[] vis) {
    VarInfo var = vis[0];

    // If we consider 'this' to be non-null obvious, then don't look for
    // these invariants.  While 'this' can clearly not be null, if 'this'
    // is a parent for all of the references to the class, those references
    // can be null and the non-null invariant becomes interesting.
    if (this_non_null_obvious) {
      if (var.isThis())
        return new DiscardInfo(this, DiscardCode.obvious,
                               "'this' can never be null in Java");
    }

    if (!var.aux.getFlag(VarInfoAux.HAS_NULL)) {
      // If it's not a number and null doesn't have special meaning...
      return new DiscardInfo(this, DiscardCode.obvious,
                     "'null' has no special meaning for " + var.name());
    }

    return super.isObviousStatically(vis);
  }

  public /*@Nullable*/ DiscardInfo isObviousDynamically(VarInfo[] vis) {
    DiscardInfo super_result = super.isObviousDynamically(vis);
    if (super_result != null) {
      return super_result;
    }

    VarInfo var = vis[0];

    Debug dlog = new Debug (getClass(), ppt, vis);

    if (logOn())
      dlog.log ("Checking IsObviousDynamically");

    // System.out.println("isObviousImplied: " + format());

    // For every EltNonZeroFloat at this program point, see if this variable is
    // an obvious member of that sequence.
    PptTopLevel parent = ppt.parent;
    for (Iterator<Invariant> itor = parent.invariants_iterator(); itor.hasNext(); ) {
      Invariant inv = itor.next();
      if ((inv instanceof EltNonZeroFloat) && inv.enoughSamples()) {
        VarInfo v2 = inv.ppt.var_infos[0];
        // System.out.println("NonZeroFloat.isObviousImplied: calling " + MemberFloat + ".isObviousMember(" + var.name + ", " + v2.name + ")");
        // Don't use isEqualToObviousMember:  that is too subtle
        // and eliminates desirable invariants such as "return != null".
        if (MemberFloat.isObviousMember(var, v2)) {
          // System.out.println("NonZeroFloat.isObviousImplied: " + MemberFloat + ".isObviousMember(" + var.name + ", " + v2.name + ") = true");
          if (logOn())
            dlog.log ("isObvDyn- true, arg is member of nonzero sequence");
          String discardString = var.name() + " is a member of the non-zero sequence " + v2.name();
          if (logOn())
            log (format() + " obviously implied from " + inv.format());
          return new DiscardInfo(this, DiscardCode.obvious, discardString);
        }
      }
    }

    if ((var.derived != null)
        && (var.derived instanceof SequenceInitialFloat)) {
      SequenceInitialFloat si = (SequenceInitialFloat) var.derived;
      if (si.index == 0) {

        // For each sequence variable, if var is an obvious member, and
        // the sequence has the same invariant, then this one is obvious.
        PptTopLevel pptt = ppt.parent;
        for (int i=0; i<pptt.var_infos.length; i++) {
          VarInfo vi = pptt.var_infos[i];
          if (MemberFloat.isObviousMember(var, vi)) {
            PptSlice1 other_slice = pptt.findSlice(vi);
            if (other_slice != null) {
              SeqIndexFloatNonEqual sine = SeqIndexFloatNonEqual.find(other_slice);
              if ((sine != null) && sine.enoughSamples()) {
                // System.out.println("NonZeroFloat.isObviousImplied true due to: " + sine.format());
                if (logOn())
                  dlog.log ("isObvDyn- true due to " + sine.format());
                String discardString = var.name() + " is a member of the non-zero sequence " + vi.name();
                return new DiscardInfo(this, DiscardCode.obvious, discardString);
              }
            }
          }
        }
      }
    }

    return null;
  }

  public boolean isSameFormula(Invariant other) {
    assert other instanceof NonZeroFloat;
    return true;
  }

  public boolean isExclusiveFormula(Invariant other) {
    if (other instanceof OneOfScalar) {
      OneOfScalar oos = (OneOfScalar) other;
      if ((oos.num_elts() == 1) && (((Long)oos.elt()).doubleValue() == 0)) {
        return true;
      }
    }
    return false;
  }

}
